When working in intensional type theory such as homotopy type theory, the notion of category has both a precategory version and a univalent category version. The same is true for other categorical structures, in particular for dagger-categories we have -precategories and univalent -categories.
A -precategory is defined in type theory using the “family of functions” definition of dagger-category. Thus, it consists of
A precategory , with type of objects and hom-sets .
For all , a function
For every , .
For every and every and , .
For every and every , .
Note that as for any precategory, there is no h-level restriction on the type . As usual in a -category, we define an isomorphism in a -precategory to be unitary if .
Let denote the type of unitary isomorphisms. The identity morphism is unitary, so there is a function
defined by induction on identity.
A -precategory is univalent (or saturated) if is an equivalence for all .
We may denote the inverse of by .
Every univalent groupoid is a univalent dagger category with .
There is a -precategory Rel of h-sets and relations (i.e. Prop-valued binary functions), where is the opposite relation of a relation . Assuming the global univalence axiom, this -category is univalent because an invertible relation is necessarily a function, and hence a bijection.
There is a -category of Hilbert spaces over the real numbers and linear maps, where is the adjoint linear map of . This is also univalent, assuming the univalence axiom.
Indeed, if the univalence axiom holds, then most naturally-occurring -categories can be proven to be univalent.
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013): Section 9.7.
Benedikt Ahrens, Paige North, Mike Shulman, and Dimitris Tsementzis, The Univalence Principle, arxiv (2021): Example 12.1.
Last revised on November 8, 2023 at 08:58:52. See the history of this page for a list of all contributions to it.